This PR is a natural continuation of, and completes, the work started in #193 and #191 on unifying categories and functors across all layers of the application. In particular, it establishes this unification at the database level, which in turn enables the unification of database queries and the associated functions and components.

As a result, a significant amount of code duplication between categories and functors is removed. It also makes it considerably easier to add new categorical structures (#4) without introducing further duplication.

Unified tables

To achieve this, the two largely redundant tables categories and functors are replaced by a single structures table containing all shared data, together with a new type field that currently is either category or functor. Similarly, the separate tables category_properties and functor_properties are replaced by a single properties table. Category-specific information is still stored in a dedicated categories table, which now contains only object and morphism data and uses a reference to the structures table as its primary key. Similarly, there is a table functors which holds functor-specific data only. For details, see the database diagram below.

This change required updates throughout the application, including the SQL schema, seed script, deduction scripts, load functions, and Svelte components.

Database diagram

Before

After

Remark

This is the third attempt at this unification of the schema. The first was never submitted as a PR, and the second was the recent attempt in #224.

Follow Up

Currently, the id is the primary key for properties. However, this cannot remain as is, since it prevents adding a property such as "cocomplete" for monoidal categories since a corresponding property already exists for categories. (A monoidal category is cocomplete when its underlying category is cocomplete and the tensor product preserves colimits in each variable, which defines a different notion.)

One option is to rename properties in a way that avoids collisions, but a more robust solution would be to use the combination of (id, type) as the primary key. This change can be done in a later PR.